$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} . lastchange($x$;$e$) $\in$ E